Nuprl Definition : ma-declm
0,22
postcript
pdf
rcv(
l
,
tg
) declared in
M
== rcv(
l
,
tg
)
dom(1of(2of(
M
)))
latex
clarification:
rcv(
l
,
tg
) declared in
M
== fpf-dom(KindDeq; rcv(
l
,
tg
); 1of(2of(
M
)))
latex
Definitions
b
,
x
dom(
f
)
,
KindDeq
,
rcv(
l
,
tg
)
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
ma-declm
origin
dom(1of(2of(M)))
dom(1of(2of(M)))
b dom(f)